$\forall$$T$:Type, $P$:($T$$\rightarrow$Prop).
\\[0ex]($\forall$$x$:$T$. SqStable($P$($x$)))
\\[0ex]$\Rightarrow$ (finite{-}type(\{$x$:$T$$\mid$ $P$($x$) \}) $\Leftrightarrow$ ($\exists$$L$:$T$ List. $\forall$$x$:$T$. $P$($x$) $\Leftrightarrow$ ($x$ $\in$ $L$)))